Lambda the Ultimate

(via Tim Bray)

Since real world applications are naturally parallel and hardware is naturally parallel, what we need is a programming model, system software, and a supporting architecture that are naturally parallel. Researchers have the rare opportunity to re-invent these cornerstones of computing, provided they simplify the efficient programming of highly parallel systems.

An interesting survey by a large and multidisciplinary group of Berkeley researchers. I think it is useful background reading for programming language researchers, even if the discussion of programming models is not up to the standards of LtU...

And yes, STM is mentioned (albeit briefly)...

Haven't seen this paper by Tim Sheard mentioned on Ltu before. As in previous papers Sheard tries to put Howard Curry to work in terms that are understandable for those that don't have a Phd in type theory.

Abstract:
Omega is an experimental system that combines features of both a programming language and a logical reasoning system. Omega is a language with an infinite hierarchy of computational levels. Terms at one level are classified (or typed) by terms at the next higher level. In this paper we report on using two different computational mechanisms. At the value level, computation is performed by reduction, and is largely unconstrained. At all higher levels, computation is performed by narrowing.

A detailed blog post on STM - and why it is a Bad Thing.

We propose programming language mechanisms to reduce redundancy in program source code. These abbreviation mechanisms, shorthands, make programs shorter and easier to write and read. In addition, we provide a framework for describing language abbreviation mechanisms.

An interesting and odd paper from Todd Proebsting (of "Proebsting's Law"fame) and Ben Zorn. If you like $_ and @_ in Perl, then you may like this, too. I can't recall seeing any other papers on this topic, so pointers are welcome.

The Metronome technology, developed at IBM Research and now available in production, solves [the problem of realtime GC] by limiting interruptions to one millisecond and spacing them evenly throughout the application's execution.2 Memory consumption is also strictly limited and predictable, since an application can't be realtime if it starts paging or throws an out-of-memory exception.

The article is primarily about the Metronome garbage collection technology, but includes a nice introduction to garbage collection and realtime terminology as well.

Programming Parallel Algorithms, Guy Blelloch. 1996.

Many constructs have been suggested for expressing parallelism in programming languages, including fork-and-join constructs, data-parallel constructs, and futures, among others. The question is which of these are most useful for specifying parallel algorithms? If we look at the parallel algorithms that are described in the literature and their pseudocode, we find that nearly all are described as parallel operations over collections of values. For example ``in parallel for each vertex in a graph, find its minimum neighbor'', or ``in parallel for each row in a matrix, sum the row''. Of course the algorithms are not this simple--they usually consist of many such parallel calls interleaved with operations that rearrange the order of a collection, and can be called recursively in parallel, as in Quicksort. This ability to operate in parallel over sets of data is often referred to as data-parallelism, and languages based on it are often referred to as data-parallel languages or collection-oriented languages. We note that many parallel languages have data-parallel features in conjunction with other forms of parallelism.

Before we come to the rash conclusion that data-parallel languages are the panacea for programming parallel algorithms, we make a distinction between flat and nested data-parallel languages. In flat data-parallel languages a function can be applied in parallel over a set of values, but the function itself must be sequential. In nested data-parallel languages any function can be applied over a set of values, including parallel functions. For example, the summation of each row of the matrix mentioned above could itself execute in parallel using a tree sum. We claim that the ability to nest parallel calls is critical for expressing algorithms in a way that matches our high-level intuition of how they work. In particular, nested parallelism can be used to implement nested loops and divide-and-conquer algorithms in parallel (five out of the seven algorithms described in this article use nesting in a crucial way).

IIRC, the team developing Fortress is putting nested data parallelism into Fortress. I think this is one of the most intriguing ways of getting heavy duty parallelism -- something that will grow ever more important as the number of cores in our computers grow.

Termination Checking with Types, Andreas Abel. 2004.

The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces lambda+mu, a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is established formally.

Recently on LtU, there has been a good deal of discussion about total functional programming, so I thought I'd link to an article that shows how to use typing to enforce termination. The main advantage of type-based approaches (as compared to analyzing the program text directly) is that the termination check is not as sensitive to the precise shape of the program; for example, you can beta-reduce a term and not alter whether the system thinks the program will terminate or not.

This paper is also nice because it provides a relatively simple example of bidirectional type checking, which is an important idea both practically (it reduces spurious type annotations and helps produce better error messages) and theoretically (it is intimately related to cut elimination).

State of the Union: Type Inference via Craig Interpolation, by Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu

The ad-hoc use of unions to encode disjoint sum types in C programs and the inability of C's type system to check the safe use of these unions is a long standing source of subtle bugs. We present a dependent type system that rigorously captures the ad-hoc protocols that programmers use to encode disjoint sums, and introduce a novel technique for automatically inferring, via Craig Interpolation, those dependent types and thus those protocols. In addition to checking the safe use of unions, the dependent type information inferred by interpolation gives programmers looking to modify or extend legacy code a precise understanding of the conditions under which some fields may be safely accessed. We present an empirical evaluation of our technique on 350KLOC of open source C code. In 80 out of 90 predicated edges (corresponding to 1472 out of 1684 union accesses), our type system is able to infer the correct dependent types. This demonstrates that our type system captures and explicates programmers' informal reasoning about unions, without requiring manual annotation or rewriting.

RZ for Constructive Mathematics in Programming by Chris Stone and Andrej Bauer.

Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.

I haven't read the paper yet, but the abstract reminded me of PADS.

Separation Logic: A Logic for Shared Mutable Data Structure, John C. Reynolds. LICS 2002

In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure.

The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a "separating conjunction" that asserts that its subformulas hold for disjoint parts of the heap, and a closely related "separating implication". Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing.

I think this paper has been mentioned several times in discussion on LtU, but never gotten an article of its own. It's a really elegant piece of work that addresses the biggest weakness of Hoare logic: that you cannot do local, modular correctness proofs of programs that use aliasable state.

(I should say my own research is on using separation logic in languages like ML or Haskell, so I am a partisan!)